COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BDB30\M1BASI30\M2CLAR30\M3SUB\M4SUP\.
C00007 ENDMK
C⊗;
\\M0BDB30;\M1BASI30;\M2CLAR30;\M3SUB;\M4SUP;\.
\F0\CFOL as a many-sorted first order logic


\J	There are two ways of restricting the ranges of variables in first order
theories.  The most straight-forward way is to introduce several distinct classes of
individual variable symbols and to broaden the notion of an interpretation so that
it includes the mention of more than one domain.  The notion of satisfiability
extends in the obvious way.  This type of formal system seems natural for some
mathematical applications.  It is the ususal way of axiomatizing vector spaces, in which there are
variables ranging over scalars and those ranging over vectors.  Also in 
Newman-Bernays-Goedel, there are two sorts of variables--one for classes and one
for sets.  This will be illustrated below.  Note that a domain by definition is non-empty.

	The second way of restricting the range of variables of a theory T is to 
introduce sorts as a conservative extension of its
latter technique whihc has been adopted in FOL.

	A \F1sort\F0 is simply a predicate on individuals whose range is non-empty.
Suppose we introduce some finite number of them S\F31\F0,...,S\F3n\F0 together with the 
axioms ∃x S\F3i\F1(x) for each i, then we can make the following additions to L\F3T\F0.
For each i, we add a countable number of wymbols for individual variables and individual 
parameters.\.


		******


\J	It now follows that without further bother that if ∃sS(s) we can use these
formulas as if they were not abbreviations at all.

I.  Justification of US.\.



		******



II. UG





		******




III.





		******








IV. 	∃G



		********


\J	It is here that we need the assumption that ∃x.S(x).\.







		********


\J	Thus if 3 is an asiom or a theorem, we are okay.  This corresponds in the 
first apprach to sorts that the Domains of Interpretations are \F1always\F0 non-empty.
(Note:  if this were not true ∀x.P(s)⊃∃x.P(s) would not be valied).

	In the proof checker this situation is guaranteed by 1) declaring some symbol 
INDCONST of that sort, 2) adding on axiom ∃x.S(s)., 3) ignoring it, in which case
when you try to ∃I you will get ∃x(S(x)⊃P(x) and messages.

	The ratio of more general than..

	Since sorts are just predicates, we can introduce a position order on them in 
the following way.  For two sorts S,T.

		MG(S,T) = ∀x(T(x)⊃S(x))

MG(S,T) is read.  S is more general than T.\.

Let MG(S,T) ∧ MG(R,S)

\JLet r1, r2 (s1,s2;t1,t2) be indices of R(S,T) and r,s,t be terms of sort R,S,T respectively.
Then we prove the following theorems.\.


		*******